Section: New Results

Model V&V and Testing

Formal MDE Foundations

Participants : Benoit Baudry, Benoit Combemale.

• Formally Tracing Executions From an Analysis Tool Back to a Domain Specific Modeling Language's Operational Semantics: in this work, we propose a formal and operational framework for tracing results back (e.g., a program crash log, or a counterexample returned by a model checker) from execution and verification tools to an original DSML's syntax and operational semantics [31] .

• A Proof Assistant Based Formalization of components in MDE: using the Coq proof assistant we propose a formalization of some operators for model fragment extraction and composition, as defined in the ReuseWare toolset [39] .

• We have developed a methodology to explicitly model the context in which a temporal property must be verified. This contextual information is expressed in the requirements, and an explicit model allows to reduce the complexity of automated verification [41] .

Pairwise testing for highly variable systems

Participants : Benoit Baudry, Aymeric Hervieu.

Variability management is a major concern for the development of software intensive systems. In particular, the explosion of variants is an issue for testing and analysis. Feature models allow to explicitly capture the variability in a formal model and get a complete view on all possible variants of the system. We have investigated pair-wise generation from feature models in order to test software product lines [36] , and to evaluate QoS contracts in variable web service compositions [38] .

Testing aspect-oriented programs

Participant : Benoit Baudry.

Aspect-oriented mechanisms introduce new risks for reliability that must be tackled by specific testing techniques in order to fully benefit from the use of this paradigm. We have investigated a monitoring mechanism of advices in an aspect-oriented program and use this information to build test cases that target faults in pointcut descriptors [18] .

Modeling model quality metrics

Participants : Benoit Baudry, Jean-Marc Jézéquel.

We have developed a model-driven measurement approach to measure models of a domain specific modeling language. The approach uses models as unique and consistent metric specifications for the automated generation of a metric tool. The benefit from applying the approach is evaluated by four case studies [20] . In particular, we have evaluated the ability of the approach to build a tool for the measurement of requirements documents [21] .